Inference at * 2 1 1 2 
Iof proof for Lemma member nth tl:



1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
5. T
6. T List
7. n:. nth_tl(n;[]) = []
  nth_tl(n;[]) = [] 

latex

 by MaAuto 

latex

 .

Definitions	, [], nth_tl(n;as), n - m, (x  l), , {x:A| B(x)} , A, False, P  Q, Void, type List, a < b, , x:A. B(x), x:AB(x), , Type, #$n, A  B, s = t, t  T
Lemmas	le wf